Nuprl Lemma : member-es-interval
0,22
postcript
pdf
es
:ES,
e
,
e'
,
ev
:E. (
ev
[
e
,
e'
])
e
ev
&
ev
e'
latex
Definitions
{
T
}
,
[
e
,
e'
]
,
P
Q
,
P
Q
,
P
Q
,
filter(
P
;
l
)
,
as
@
bs
,
before(
e
)
,
es-ble{i:l}(
es
;
e
;
e'
)
,
(
x
l
)
,
b
,
P
&
Q
,
e
e'
,
Prop
,
(
e
<loc
e'
)
,
P
Q
,
False
,
E
,
x
:
A
.
B
(
x
)
,
t
T
,
ES
Lemmas
event
system
wf
,
es-E
wf
,
false
wf
,
es-locl
wf
,
l
member
wf
,
assert
wf
,
es-le
wf
,
es-ble
wf
,
es-before
wf
,
append
wf
,
filter
wf
,
assert-es-ble
,
and
functionality
wrt
iff
,
iff
functionality
wrt
iff
,
nil
member
,
or
functionality
wrt
iff
,
cons
member
,
member-es-before
,
member
append
,
member
filter
origin